Example 4 in [Duran, Lucas, Marché, Meseguer & Urbain - PEPM'04]

Summary: Ex4_DLMMU04

• TPDB format
• OBJ format
• Negative results:
  1. Lucas'

Ex4_DLMMU04 in TPDB format ( Ex4_DLMMU04.trs):

(VAR T IL N L M)
(STRATEGY CONTEXTSENSITIVE 
  (and 1 2)
  (tt)
  (isNatIList)
  (isNatList)
  (isNat)
  (0)
  (s 1)
  (length 1)
  (zeros)
  (cons 1)
  (nil)
  (take 1 2)
  (uTake1 1)
  (uTake2 1)
  (uLength 1)
)
(RULES 
and(tt,T) -> T
isNatIList(IL) -> isNatList(IL)
isNat(0) -> tt
isNat(s(N)) -> isNat(N)
isNat(length(L)) -> isNatList(L)
isNatIList(zeros) -> tt
isNatIList(cons(N,IL)) -> and(isNat(N),isNatIList(IL))
isNatList(nil) -> tt
isNatList(cons(N,L)) -> and(isNat(N),isNatList(L))
isNatList(take(N,IL)) -> and(isNat(N),isNatIList(IL))
zeros -> cons(0,zeros)
take(0,IL) -> uTake1(isNatIList(IL))
uTake1(tt) -> nil
take(s(M),cons(N,IL)) -> uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL)
uTake2(tt,M,N,IL) -> cons(N,take(M,IL))
length(cons(N,L)) -> uLength(and(isNat(N),isNatList(L)),L)
uLength(tt,L) -> s(length(L))
)

The CS-TRS in OBJ format (file Ex4_DLMMU04.obj):

obj Ex4_DLMMU04 is
  sort S .
  op and : S S -> S .
  op tt : -> S .
  op isNatIList : S -> S [strat (0)] .
  op isNatList : S -> S [strat (0)] .
  op isNat : S -> S [strat (0)] .
  op 0 : -> S .
  op s : S -> S .
  op length : S -> S .
  op zeros : -> S .
  op cons : S S -> S [strat (1 0)] .
  op nil : -> S .
  op take : S S -> S .
  op uTake1 : S -> S .
  op uTake2 : S S S S -> S [strat (1 0)] .
  op uLength : S S -> S [strat (1 0)] .
  vars T IL N L M : S .
  eq and(tt,T) = T .
  eq isNatIList(IL) = isNatList(IL) .
  eq isNat(0) = tt .
  eq isNat(s(N)) = isNat(N) .
  eq isNat(length(L)) = isNatList(L) .
  eq isNatIList(zeros) = tt .
  eq isNatIList(cons(N,IL)) = and(isNat(N),isNatIList(IL)) .
  eq isNatList(nil) = tt .
  eq isNatList(cons(N,L)) = and(isNat(N),isNatList(L)) .
  eq isNatList(take(N,IL)) = and(isNat(N),isNatIList(IL)) .
  eq zeros = cons(0,zeros) .
  eq take(0,IL) = uTake1(isNatIList(IL)) .
  eq uTake1(tt) = nil .
  eq take(s(M),cons(N,IL)) = uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL) .
  eq uTake2(tt,M,N,IL) = cons(N,take(M,IL)) .
  eq length(cons(N,L)) = uLength(and(isNat(N),isNatList(L)),L) .
  eq uLength(tt,L) = s(length(L)) .
endo

Negative results

1. The µ-termination of Ex4_DLMMU04 cannot be proved by using Lucas' transformation. The TRS Ex4_DLMMU04_L:

   and(tt,T) -> T
   isNatIList -> isNatList
   isNat -> tt
   isNat -> isNat
   isNat -> isNatList
   isNatIList -> tt
   isNatIList -> and(isNat,isNatIList)
   isNatList -> tt
   isNatList -> and(isNat,isNatList)
   isNatList -> and(isNat,isNatIList)
   zeros -> cons(0)
   take(0,IL) -> uTake1(isNatIList)
   uTake1(tt) -> nil
   take(s(M),cons(N)) -> uTake2(and(isNat,and(isNat,isNatIList)))
   uTake2(tt) -> cons(N)
   length(cons(N)) -> uLength(and(isNat,isNatList))
   uLength(tt) -> s(length(L))
   
   

   contains extra variables.